 $LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
 require 'ext_pr1_v4'

# Uhr mit drei verschiedenen Implementationen und der Möglichkeit verschiedener
# Umrechnungen in 5 Einzelschritten
# 
# clock24   == 24 Stunden Zeitanzeige
# clock12   == 12 Stunden AM und PM Anzeige
# clockSec  == Zeitanzeige in Sekunden

MIN_IN_SEC = 60
HOUR_IN_MIN = 60
DAY_IN_HOUR = 24
HOUR_IN_SEC = HOUR_IN_MIN * MIN_IN_SEC
DAY_IN_SEC = DAY_IN_HOUR * HOUR_IN_SEC
HALF_DAY_IN_SEC = DAY_IN_SEC / 2
HALF_DAY = DAY_IN_HOUR/2

# Schritte:
# Schritt 1: 
# Sekundenuhr
# 
# ClockSec ::= ClockSec[:day_sec] :: SecDay

 def_class(:ClockSec,[:day_sec]){
   def invariant?() 
    day_sec?(day_sec)
   end
   
   # clock_sec_add ::= (sec1, sec2) :: Nat x Nat -> Nat
  # Test {(21, 19) = 40, (21, -19) = Err, (21, "Hallo") = Err, (21, 19.0) = Err,
  #       ("Hallo", 19) = Err, (21.0, 19) = Err, (-21, 19) = Err }
  def clock_sec_add(sec2)
    check_pre((sec2.clock_sec?))
     ClockSec[self.day_sec + sec2.day_sec]
  end
  
  # clock_sec_sub ::= (sec1, sec2) :: Nat x Nat -> Nat
  # Test {(21, 19) = Err, (19, 21) = 2, (21, -19) = Err, (21, "Hallo") = Err, 
  #       (21, 19.0) = Err, ("Hallo", 19) = Err, (21.0, 19) = Err, (-21, 19) = Err }

  def clock_sec_sub(sec2)
    check_pre((sec2.clock_sec? and self.day_sec >= sec2.day_sec))
    ClockSec[self.day_sec - sec2.day_sec]
  end
  
  # clock_sec_succ ::= (sec) :: Nat -> Nat
  # Test { (18) = 19, (18.0) = Err, ("Hallo") = Err, (-18) = Err }

  def clock_sec_succ()
    ClockSec[self.day_sec.succ]

  end
  
  # clock_sec_pred ::= (sec) :: Nat -> Nat
  # Test { (18) = 17, (18.0) = Err, ("Hallo") = Err, (-18) = Err }

  def clock_sec_pred()
    ClockSec[self.day_sec.pred]
  end
  
  #Konvertierung von ClockSec zu Clock24
  # clock_sec_to_clock_24 ::= (clock) :: ClockSec <-> Clock24
  # Test {clock_sec_to_clock_24(ClockSec[43200]=>Clock24[12,0,0], clock_sec_to_clock_24(ClockSec[45296])=>Clock24[12,34,56],
  # clock_sec_to_clock24(ClockSec[86400])=>Err, clock_sec_to_clock24(ClockSec[86401])=>Err, clock_sec_to_clock24(ClockSec[-12])=>Err,
  # clock_sec_to_clock24(ClockSec[12.0])=>Err, clock_sec_to_clock24(ClockSec["Hallo"])=>Err}

  def clock_sec_to_clock_24()
    check_pre((self.clock_sec?))
    hour24, hour_carry = self.day_sec.divmod(HOUR_IN_SEC)
    min, sec = hour_carry.divmod(MIN_IN_SEC)

    Clock24[hour24, min, sec]
  end
  
  #Konvertierung von ClockSec zu Clock12
  #clock_sec_to_clock_12 ::= (clock) :: ClockSec <-> Clock12
  # Test {clock_sec_to_clock_12(ClockSec[43200])=>Clock12[:AM,12,0,0], clock_sec_to_clock_12(ClockSec[43201])=>Clock12[:PM,12,0,1],
  # clock_sec_to_clock_12(ClockSec[3540])=>Clock12[:AM,12,59,0], clock_sec_to_clock_12(ClockSec[1])=>Clock12[:AM,12,0,1],
  # clock_sec_to_clock12(ClockSec[86400])=>Err, clock_sec_to_clock12(ClockSec[86401])=>Err, clock_sec_to_clock12(ClockSec[-12])=>Err,
  # clock_sec_to_clock12(ClockSec[12.0])=>Err, clock_sec_to_clock12(ClockSec["Hallo"])=>Err}
  #def clock_sec_to_clock_12(clocksec)
  #  check_pre((clocksec.clock_sec?))
  #  (clocksec.day_sec <= HALF_DAY_IN_SEC and clocksec.day_sec != 0) ? func_am(clocksec.day_sec) : func_pm(clocksec.day_sec)
  #end
  #def func_pm(v)
  #  sec = v.divmod(MIN_IN_SEC)
  #  min = (sec[0]).divmod(HOUR_IN_MIN)
  #  Clock12[:PM, min[0] <= HALF_DAY ? min[0] : min[0] - HALF_DAY, min[1], sec[1]]
  #end
  #def func_am(v)
  #  sec = v.divmod(MIN_IN_SEC)
  #  min = (sec[0]).divmod(HOUR_IN_MIN)
  #  Clock12[:AM, min[0] > 0 ? min[0] : HALF_DAY, min[1], sec[1]]
  #end

  def clock_sec_to_clock_12()
    check_pre((self.clock_sec?))
    hour24, hour_carry = self.day_sec.divmod(HOUR_IN_SEC)
    min, sec = hour_carry.divmod(MIN_IN_SEC)
    halve = hour24 % HALF_DAY
    hour12 = hour24 > HALF_DAY-1 ? (hour24-HALF_DAY) : hour24
    Clock12[ halve == 1 ? :PM : :AM, hour12, min, sec]
  end
 }
 
 def day_sec?(param)
  param.int? and param.in?(0...DAY_IN_SEC)
 end


def check(param)
  check_pre((param.clock_sec?))
end

#Schritt 2:
#24 Stunden Uhr
#
# Clock24 ::= Clock24[hour24,min,sec] :: Hour24 x Min x Sec
#
def_class(:Clock24,[:hour24,:min,:sec]){
  def invariant?()
    hour24?(hour24) and min?(min) and sec?(sec)
  end
  #Schritt 3:
  #Konvertierung von Clock24 zu ClockSec
  # clock_24_to_clock_sec ::= (clock) :: Clock24 <-> ClockSec
  # Test { (Clock24[1, 0, 0]=>3600, Clock24[23, 0, 0]=>82800, Clock24[0, 59, 0]=>3540,
  # Clock24[0, 0, 59]=>59, Clock24[24, 0, 0]=>Err, Clock24[0, 60, 0]=>Err, Clock24[0, 0, 60]=>Err,
  # Clock24["Hallo", 0, 0]=>Err, Clock24[0, "Hallo", 0]=>Err, Clock24[0, 0, "Hallo"]=>Err, 
  # Clock24[23.0, 0, 0]=>Err, Clock24[0, 59.0, 0]=>Err, Clock24[0, 0, 59.0]=>Err, Clock24[-23, 0, 0]=>Err,
  # Clock24[0, -59, 0]=>Err, Clock24[0, 0, -59]=>Err}
  def to_clock_sec()
    sec_temp1 = self.hour24 * HOUR_IN_SEC
    sec_temp2 = self.min * MIN_IN_SEC
    sec_temp3 = self.sec
    ClockSec[sec_temp1 + sec_temp2 + sec_temp3]
  end
  
  #Konvertierung von Clock 24 auf Clock 12
  #clock_24_to_clock_12 ::= (clock) :: Clock24 <-> Clock12
  # Test {clock_24_to_clock_12(Clock24[12,0,0])=>Clock12[:AM,12,0,0], clock_24_to_clock_12(Clock24[12,0,1])=>Clock12[:PM,12,0,1],
  # clock_24_to_clock_12(Clock24[0,59,0])=>Clock12[:AM,12,59,0], clock_24_to_clock_12(Clock24[0,0,1])=>Clock12[:AM,12,0,1],
  # clock_24_to_clock_12(Clock24[12,23,48])=>Clock12[:PM,12,23,48], clock_24_to_clock_12(Clock24[24,0,0])=>Err, 
  # clock_24_to_clock_12(Clock24[23,60,0])=>Err, clock_24_to_clock_12(Clock24[23,0,60])=>Err, clock_24_to_clock_12(Clock24[23.0,0,0])=>Err,
  # clock_24_to_clock_12(Clock24[23,0.0,0])=>Err, clock_24_to_clock_12(Clock24[23,0,0.0])=>Err, clock_24_to_clock_12(Clock24["Hallo",0,0])=>Err,
  # clock_24_to_clock_12(Clock24[23,"Hallo",0])=>Err, clock_24_to_clock_12(Clock24[23,0,"Valium"])=>Err}
  def clock_24_to_clock_12()
    ClockSec[self.to_clock_sec()].clock_sec_to_clock_12()
  end
}
def hour24?(param) param.int? and param.in?(0...DAY_IN_HOUR) end 
def min?(param) param.int? and param.in?(0...HOUR_IN_MIN) end 
def sec?(param) param.int? and param.in?(0...MIN_IN_SEC) end 
#12 Stunden Uhr
#
# Clock12 ::= Clock12[halve,hour12,min,sec] :: Halve x Hour12 x Min x Sec
def_class(:Clock12,[:halve,:hour12,:min,:sec]){
  def invariant?()
   halve?(halve) and hour12?(hour12) and min?(min) and sec?(sec)
  end
  
  #Konvertierung von Clock12 zu ClockSec
  # clock_12_to_clock_sec ::= (clock) :: Clock12 <-> ClockSec
  # Test {Clock12[:AM, 1, 0, 0]=>3600, Clock12[:PM, 11, 0, 0]=>82800, Clock12[:AM, 11, 0, 0]=>39600,
  # Clock12[:AM, 12, 59, 0]=>3540, Clock12[:PM, 12, 59, 0]=>56740, Clock12[:AM, 12, 0, 59]=>59
  # Clock12[:AM, 11, 0, 0]=>39600, Clock12[:PM, 11, 0, 0]=>82800, Clock12[:AM, 13, 0, 0]=>Err,
  # Clock12[:AM, 0, 60, 0]=>Err, Clock12[:AM, 0, 0, 60]=>Err, Clock12[:AM, "Hallo", 0, 0]=>Err,
  # Clock12[:AM, 0, "Hallo", 0]=>Err, Clock12[:AM, 0, 0, "Hallo]=>Err, Clock12[:AM, 13.0, 0, 0]=>Err,
  # Clock12[:AM, 0, 59.0, 0]=>Err, Clock12[:AM, 0, 0, 59.0]=>Err, Clock12[:AM, -13, 0, 0]=>Err,
  # Clock12[:AM, 0, -59, 0]=>Err, Clock12[:AM, 0, 0, -59]=>Err, Clock12[:PM, 13, 0, 0]=>Err,
  # Clock12[:PM, 0, 60, 0]=>Err, Clock12[:PM, 0, 0, 60]=>Err, Clock12[:PM, "Hallo", 0, 0]=>Err,
  # Clock12[:PM, 0, "Hallo", 0]=>Err, Clock12[:PM, 0, 0, "Hallo]=>Err, Clock12[:PM, 13.0, 0, 0]=>Err,
  # Clock12[:PM, 0, 59.0, 0]=>Err, Clock12[:PM, 0, 0, 59.0]=>Err, Clock12[:PM, -13, 0, 0]=>Err,
  # Clock12[:PM, 0, -59, 0]=>Err, Clock12[:PM, 0, 0, -59]=>Err}
  def to_clock_sec()
    sec_temp1 = ((self.halve == :AM ? 0 : 12) + self.hour12) * HOUR_IN_SEC 
    sec_temp2 = self.min * MIN_IN_SEC
    sec_temp3 = self.sec
    ClockSec[sec_temp1 + sec_temp2 + sec_temp3]
  end
}
def halve?(param) param == :AM or param == :PM end
# NULLFEHLER IST HIER! WENN VON 1 dann FEHLER mit 12,0,0 sonst Fehler da = Uhr nicht existent bei AM und PM
def hour12?(param) param.int? and param.in?(1...(HALF_DAY+1)) end 
def min?(param) param.int? and param.in?(0...HOUR_IN_MIN) end 
def sec?(param) param.int? and param.in?(0...MIN_IN_SEC) end 


#Konvertierung von Clock 12 auf Clock 24
#clock_12_to_clock_24 ::= (clock) :: Clock12 <-> Clock24
# Test {clock_12_to_clock_24(Clock12[:AM,12,0,0])=>Clock24[12,0,0], clock_12_to_clock_24(Clock12[:PM,12,0,1])=>Clock24[12,0,1],
# clock_12_to_clock_24(Clock12[:AM,12,59,0])=>Clock24[0,59,0], clock_12_to_clock_24(Clock12[:AM,12,0,1])=>Clock24[0,0,1],
# clock_12_to_clock_24(Clock12[:PM,12,0,0])=>Clock24[0,0,0], clock_12_to_clock_24(Clock12[:PM,12,23,48])=>Clock24[12,23,48],
# clock_12_to_clock_24(Clock12[:AM,13, 0, 0])=>Err, clock_12_to_clock_24(Clock12[:AM,0, 60, 0])=>Err, 
# clock_12_to_clock_24(Clock12[:AM,0, 0, 60])=>Err, clock_12_to_clock_24(Clock12[:AM,"Hallo", 0, 0])=>Err, 
# clock_12_to_clock_24(Clock12[:AM,0, "hallo", 0])=>Err, clock_12_to_clock_24(Clock12[:AM,0, 0, "ahhhh"])=>Err, 
# clock_12_to_clock_24(Clock12[:AM,13.0, 0, 0])=>Err, clock_12_to_clock_24(Clock12[:AM,0, 59.0, 0])=>Err,
# clock_12_to_clock_24(Clock12[:AM,0,0, 59.0])=>Err, clock_12_to_clock_24(Clock12[:AM,-13, 0, 0])=>Err,
# clock_12_to_clock_24(Clock12[:AM,0, -59, 0])=>Err, clock_12_to_clock_24(Clock12[:AM,0, 0, -59])=>Err, 
# clock_12_to_clock_24(Clock12[:PM,13, 0, 0])=>Err, clock_12_to_clock_24(Clock12[:PM,0, 60, 0])=>Err, 
# clock_12_to_clock_24(Clock12[:PM,0, 0, 60])=>Err, clock_12_to_clock_24(Clock12[:PM,"Hallo", 0, 0])=>Err,
# clock_12_to_clock_24(Clock12[:PM,0, "hallo", 0])=>Err, clock_12_to_clock_24(Clock12[:PM,0, 0, "ahhhh"])=>Err,
# clock_12_to_clock_24(Clock12[:PM,13.0, 0, 0])=>Err, clock_12_to_clock_24(Clock12[:PM,0, 59.0, 0])=>Err, 
# clock_12_to_clock_24(Clock12[:PM,0,0, 59.0])=>Err, clock_12_to_clock_24(Clock12[:PM,-13, 0, 0])=>Err,
# clock_12_to_clock_24(Clock12[:PM,0, -59, 0])=>Err, clock_12_to_clock_24(Clock12[:PM,0, 0, -59])=>Err}
def clock_12_to_clock_24(clock12)
  clock_sec_to_clock_24(clock_12_to_clock_sec(clock12))
end

#Schritt 4:
#Konvertierungen:
#to_clock_24 ::= (clock) :: Clock -> Clock24

def to_clock_24 (value)
  if    value.clock_sec? then clock_sec_to_clock_24(value)
  elsif value.clock12?   then clock_12_to_clock_24(value)
  elsif value.clock24?   then value
  else  check_pre((false))
  end
end

#to_clock_12 ::= (clock) :: Clock -> Clock12

def to_clock_12 (value)
  if    value.clock_sec? then clock_sec_to_clock_12(value)
  elsif value.clock24?   then clock_24_to_clock_12(value)
  elsif value.clock12?   then value
  else  check_pre((false))
  end
end

#to_clock_sec ::= (clock) :: Clock -> ClockSec

def to_clock_sec (value)
  if    value.clock12? then clock_12_to_clock_sec(value)
  elsif value.clock24?   then clock_24_to_clock_sec(value)
  elsif value.clock_sec?   then value
  else  check_pre((false))
  end
end

#Allgemeine Konvertierung
#
#to_clock ::= (proto,value) :: Clock x Clock -> Clock ::
#                              (Clock24 x Clock -> Clock24 |
#                               Clock12 x Clock -> Clock12 |
#                               ClockSec x Clock -> ClockSec)
# test {
# to_clock(:Clock24, ClockSec[3600])=>Clock24[1,0,0], to_clock(:Clock24, ClockSec[43200])=>Clock24[12,0,0],
# to_clock(:Clock24, ClockSec[0])=>Clock24[0,0,0], to_clock(:Clock24, Clock12[:AM,1,0,0])=>Clock24[1,0,0],
# to_clock(:Clock24, Clock12[:PM,12,0,1])=>Clock24[12,0,1], to_clock(:Clock24, Clock12[:AM,12,0,1])=>Clock24[0,0,1],
# to_clock(:Clock24, Clock12[:PM,12,0,0])=>Clock24[0,0,0], to_clock(:Clock24, Clock24[1,0,0])=>Clock24[1,0,0],
# to_clock(:Clock24, Clock24[12,0,0])=>Clock24[12,0,0], to_clock(:Clock24, Clock24[23,45,59])=>Clock24[23,45,59],
# to_clock(:Clock24, Clock24[0,0,0])=>Clock24[0,0,0], to_clock(:Clock24,ClockSec[86400])=>Err, to_clock(:Clock24,ClockSec["Hallo"])=>Err,
# to_clock(:Clock24,ClockSec[12.0])=>Err, to_clock(:Clock24,ClockSec[-43200])=>Err, to_clock(:Clock24,Clock12[:AM,13,0,0])=>Err,
# to_clock(:Clock24,Clock12[:PM,13,0,0])=>Err, to_clock(:Clock24,Clock12[:AM,12,60,0])=>Err, to_clock(:Clock24,Clock12[:PM,12,60,0])=>Err,
# to_clock(:Clock24,Clock12[:AM,12,0,60])=>Err, to_clock(:Clock24,Clock12[:PM,12,0,60])=>Err, to_clock(:Clock24,Clock12[:AM,12.0,0,0])=>Err,
# to_clock(:Clock24,Clock12[:PM,12.0,0,0])=>Err, to_clock(:Clock24,Clock12[:AM,12,0.0,0])=>Err, to_clock(:Clock24,Clock12[:PM,12,0.0,0])=>Err,
# to_clock(:Clock24,Clock12[:AM,12,0,0.0])=>Err, to_clock(:Clock24,Clock12[:PM,12,0,0.0])=>Err, to_clock(:Clock24,Clock12[:AM,"Hallo",0,0])=>Err,
# to_clock(:Clock24,Clock12[:PM,"Hallo",0,0])=>Err, to_clock(:Clock24,Clock12[:AM,12,"Hallo",0])=>Err, to_clock(:Clock24,Clock12[:PM,12,"Hallo",0])=>Err,
# to_clock(:Clock24,Clock12[:AM,12,0,"Hallo"])=>Err, to_clock(:Clock24,Clock12[:PM,12,0,"Hallo"])=>Err, to_clock(:Clock24,Clock12[:AM,-12,0,0])=>Err,
# to_clock(:Clock24,Clock12[:PM,-12,0,0])=>Err, to_clock(:Clock24,Clock12[:AM,12,-1,0])=>Err, to_clock(:Clock24,Clock12[:PM,12,-1,0])=>Err,
# to_clock(:Clock24,Clock12[:AM,12,0,-1])=>Err, to_clock(:Clock24,Clock12[:PM,12,0,-1])=>Err, to_clock(:Clock24,Clock24[24,0,0])=>Err, 
# to_clock(:Clock24,Clock24[23,60,0])=>Err, to_clock(:Clock24,Clock24[23,0,60])=>Err, to_clock(:Clock24,Clock24[-23,0,0])=>Err, 
# to_clock(:Clock24,Clock24[23,-1,0])=>Err, to_clock(:Clock24,Clock24[23,0,-1])=>Err, to_clock(:Clock24,Clock24[23.0,0,0])=>Err, 
# to_clock(:Clock24,Clock24[23,59.0,0])=>Err, to_clock(:Clock24,Clock24[23,0,59.0])=>Err, to_clock(:Clock24,Clock24["Hallo",0,0])=>Err,
# to_clock(:Clock24,Clock24[23,"Hallo",0])=>Err, to_clock(:Clock24,Clock24[23,0,"Hallo"])=>Err, to_clock(:Clock12, ClockSec[3600])=>Clock12[:AM,1,0,0],
# to_clock(:Clock12, ClockSec[43200])=>Clock12[:AM,12,0,0], to_clock(:Clock12, ClockSec[43201])=>Clock12[:PM,12,0,1], to_clock(:Clock12, ClockSec[1])=>Clock12[:AM,12,0,1],
# to_clock(:Clock12, ClockSec[0])=>Clock12[:PM,12,0,0], to_clock(:Clock12, Clock24[1,0,0])=>Clock12[:AM,1,0,0],
# to_clock(:Clock12, Clock24[12,0,0])=>Clock12[:AM,12,0,0], to_clock(:Clock12, Clock24[12,0,1])=>Clock12[:PM,12,0,1], 
# to_clock(:Clock12, Clock24[0,0,1])=>Clock12[:AM,12,0,1], to_clock(:Clock12, Clock12[:AM,1,0,0])=>Clock12[:AM,1,0,0],
# to_clock(:Clock12, Clock12[:AM,12,0,0])=>Clock12[:AM,12,0,0], to_clock(:Clock12, Clock12[:PM,12,0,1])=>Clock12[:PM,12,0,1],
# to_clock(:Clock12, Clock12[:AM,12,0,1])=>Clock12[:AM,12,0,1], to_clock(:Clock12,Clock12[:AM,13,0,0])=>Err,
# to_clock(:Clock12,Clock12[:PM,13,0,0])=>Err, to_clock(:Clock12,Clock12[:AM,12,60,0])=>Err, to_clock(:Clock12,Clock12[:PM,12,60,0])=>Err,
# to_clock(:Clock12,Clock12[:AM,12,0,60])=>Err, to_clock(:Clock12,Clock12[:PM,12,0,60])=>Err, to_clock(:Clock12,Clock12[:AM,12.0,0,0])=>Err,
# to_clock(:Clock12,Clock12[:PM,12.0,0,0])=>Err, to_clock(:Clock12,Clock12[:AM,12,0.0,0])=>Err, to_clock(:Clock12,Clock12[:PM,12,0.0,0])=>Err,
# to_clock(:Clock12,Clock12[:AM,12,0,0.0])=>Err, to_clock(:Clock12,Clock12[:PM,12,0,0.0])=>Err, to_clock(:Clock12,Clock12[:AM,"Hallo",0,0])=>Err,
# to_clock(:Clock12,Clock12[:PM,"Hallo",0,0])=>Err, to_clock(:Clock12,Clock12[:AM,12,"Hallo",0])=>Err, to_clock(:Clock12,Clock12[:PM,12,"Hallo",0])=>Err,
# to_clock(:Clock12,Clock12[:AM,12,0,"Hallo"])=>Err, to_clock(:Clock12,Clock12[:PM,12,0,"Hallo"])=>Err, to_clock(:Clock12,Clock12[:AM,-12,0,0])=>Err,
# to_clock(:Clock12,Clock12[:PM,-12,0,0])=>Err, to_clock(:Clock12,Clock12[:AM,12,-1,0])=>Err, to_clock(:Clock12,Clock12[:PM,12,-1,0])=>Err,
# to_clock(:Clock12,Clock12[:AM,12,0,-1])=>Err, to_clock(:Clock12,Clock12[:PM,12,0,-1])=>Err, to_clock(:Clock12,Clock24[24,0,0])=>Err, 
# to_clock(:Clock12,Clock24[23,60,0])=>Err, to_clock(:Clock12,Clock24[23,0,60])=>Err, to_clock(:Clock12,Clock24[-23,0,0])=>Err,
# to_clock(:Clock12,Clock24[23,-1,0])=>Err, to_clock(:Clock12,Clock24[23,0,-1])=>Err, to_clock(:Clock12,Clock24[23.0,0,0])=>Err,
# to_clock(:Clock12,Clock24[23,59.0,0])=>Err, to_clock(:Clock12,Clock24[23,0,59.0])=>Err, to_clock(:Clock12,Clock24["Hallo",0,0])=>Err,
# to_clock(:Clock12,Clock24[23,"Hallo",0])=>Err, to_clock(:Clock12,Clock24[23,0,"Hallo"])=>Err, to_clock(:Clock12,ClockSec[86400])=>Err,
# to_clock(:Clock12,ClockSec["Hallo"])=>Err, to_clock(:Clock12,ClockSec[12.0])=>Err, to_clock(:Clock12,ClockSec[-43200])=>Err, to_clock(:ClockSec, ClockSec[3600])=>ClockSec[3600], to_clock(:ClockSec, ClockSec[43200])=>ClockSec[43200], to_clock(:ClockSec, Clock24[12,0,0]))=>ClockSec[43200]
#to_clock(:ClockSec, Clock24[1,0,0]=>ClockSec[3600], to_clock(:ClockSec, Clock12[:AM,12,0,0])=>ClockSec[43200], to_clock(:ClockSec, Clock12[:PM,12,0,1])=>ClockSec[43201]
#to_clock(:ClockSec, Clock12[:AM,12,0,1])=>ClockSec[1], to_clock(:ClockSec,Clock12[:AM,13,0,0])=> Err, to_clock(:ClockSec,Clock12[:PM,13,0,0])=> Err, 
#to_clock(:ClockSec,Clock12[:AM,12,60,0]=> Err, to_clock(:ClockSec,Clock12[:PM,12,60,0])=> Err, to_clock(:ClockSec,Clock12[:AM,12,0,60]))=> Err, to_clock(:ClockSec,Clock12[:PM,12,0,60])=> Err,
#to_clock(:ClockSec,Clock12[:AM,12.0,0,0])=> Err, to_clock(:ClockSec,Clock12[:PM,12.0,0,0])=> Err, to_clock(:ClockSec,Clock12[:AM,12,0.0,0])=> Err, to_clock(:ClockSec,Clock12[:PM,12,0.0,0])=> Err,
#to_clock(:ClockSec,Clock12[:AM,12,0,0.0])=> Err, to_clock(:ClockSec,Clock12[:PM,12,0,0.0])=> Err, to_clock(:ClockSec,Clock12[:AM,"Hallo",0,0])=> Err, 
#to_clock(:ClockSec,Clock12[:PM,"Hallo",0,0])=> Err, to_clock(:ClockSec,Clock12[:AM,12,"Hallo",0])=> Err, to_clock(:ClockSec,Clock12[:PM,12,"Hallo",0])=> Err, 
#to_clock(:ClockSec,Clock12[:AM,12,0,"Hallo"])=> Err, to_clock(:ClockSec,Clock12[:PM,12,0,"Hallo"])=> Err, to_clock(:ClockSec,Clock12[:AM,-12,0,0])=> Err, 
#to_clock(:ClockSec,Clock12[:PM,-12,0,0])=> Err, to_clock(:ClockSec,Clock12[:AM,12,-1,0])=> Err, to_clock(:ClockSec,Clock12[:PM,12,-1,0])=> Err, to_clock(:ClockSec,Clock12[:AM,12,0,-1])=> Err, 
#to_clock(:ClockSec,Clock12[:PM,12,0,-1])=> Err, to_clock(:ClockSec,Clock24[24,0,0])=> Err, to_clock(:ClockSec,Clock24[23,60,0])=> Err, to_clock(:ClockSec,Clock24[23,0,60])=> Err, 
#to_clock(:ClockSec,Clock24[-23,0,0])=> Err, to_clock(:ClockSec,Clock24[23,-1,0])=> Err, to_clock(:ClockSec,Clock24[23,0,-1])=> Err, to_clock(:ClockSec,Clock24[23.0,0,0])=> Err, 
#to_clock(:ClockSec,Clock24[23,59.0,0])=> Err, to_clock(:ClockSec,Clock24[23,0,59.0])=> Err, to_clock(:ClockSec,Clock24["Hallo",0,0])=> Err, to_clock(:ClockSec,Clock24[23,"Hallo",0])=> Err, 
#to_clock(:ClockSec,Clock24[23,0,"Hallo"])=> Err, to_clock(:ClockSec,ClockSec[86400])=> Err, to_clock(:ClockSec,ClockSec["Hallo"])=> Err, to_clock(:ClockSec,ClockSec[12.0])=> Err, 
#to_clock(:ClockSec,ClockSec[-43200])=> Err}
def to_clock(proto, valium)
  
    if    proto.clock_sec?  then to_clock_sec(valium)
    elsif proto.clock24?    then to_clock_24(valium)
    elsif proto.clock12?    then to_clock_12(valium)
    else check_pre((false))
    end
end
 
#Schritt 5
#
# 
# clock_add ::= (clock1,clock2) ::
#                               (Clock24 x Clock -> Clock24 |
#                                Clock12 x Clock -> Clock12 |
#                                ClockSec x Clock -> ClockSec)
#Test { clock_add(ClockSec[39600], ClockSec[3600])=>ClockSec[43200], clock_add(ClockSec[39600], Clock12[:AM,1,0,0])=>ClockSec[43200],
# clock_add(ClockSec[39600], Clock24[1,0,0])=>ClockSec[43200], clock_add(Clock24[11,0,0], ClockSec[3600])=>Clock24[12,0,0],
# clock_add(Clock24[11,0,0], ClockSec[3600])=>Clock24[12,0,0], clock_add(Clock24[11,0,0], Clock12[:AM,1,0,0])=>Clock24[12,0,0],
# clock_add(Clock24[11,0,0], Clock24[1,0,0])=>Clock24[12,0,0], clock_add(Clock12[:AM,11,0,0], ClockSec[3600])=>Clock12[:AM,12,0,0],
# clock_add(Clock12[:AM,11,0,0], Clock12[:AM,1,0,0])=>Clock12[:AM,12,0,0], clock_add(Clock12[:AM,11,0,0], Clock24[1,0,0])=>Clock12[:AM,12,0,0],
# clock_add(Clock24[11,0,0],Clock12[:AM,13,0,0]))=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,13,0,0])=>Err, 
# clock_add(Clock24[11,0,0],Clock12[:AM,12,60,0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,60,0])=>Err,
# clock_add(Clock24[11,0,0],Clock12[:AM,12,0,60])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,0,60])=>Err, 
# clock_add(Clock24[11,0,0],Clock12[:AM,12.0,0,0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12.0,0,0])=>Err, 
# clock_add(Clock24[11,0,0],Clock12[:AM,12,0.0,0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,0.0,0])=>Err, 
# clock_add(Clock24[11,0,0],Clock12[:AM,12,0,0.0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,0,0.0])=>Err,
# clock_add(Clock24[11,0,0],Clock12[:AM,"Hallo",0,0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,"Hallo",0,0])=>Err,
# clock_add(Clock24[11,0,0],Clock12[:AM,12,"Hallo",0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,"Hallo",0])=>Err,
# clock_add(Clock24[11,0,0],Clock12[:AM,12,0,"Hallo"])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_add(Clock24[11,0,0],Clock12[:AM,-12,0,0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,-12,0,0])=>Err, 
# clock_add(Clock24[11,0,0],Clock12[:AM,12,-1,0])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,-1,0])=>Err,
# clock_add(Clock24[11,0,0],Clock12[:AM,12,0,-1])=>Err, clock_add(Clock24[11,0,0],Clock12[:PM,12,0,-1])=>Err,
# clock_add(Clock24[11,0,0],Clock24[24,0,0])=>Err, clock_add(Clock24[11,0,0],Clock24[23,60,0])=>Err,
# clock_add(Clock24[11,0,0],Clock24[23,0,60])=>Err, clock_add(Clock24[11,0,0],Clock24[-23,0,0])=>Err,
# clock_add(Clock24[11,0,0],Clock24[23,-1,0])=>Err, clock_add(Clock24[11,0,0],Clock24[23,0,-1])=>Err, clock_add(Clock24[11,0,0],Clock24[23.0,0,0])=>Err,
# clock_add(Clock24[11,0,0],Clock24[23,59.0,0])=>Err, clock_add(Clock24[11,0,0],Clock24[23,0,59.0])=>Err, 
# clock_add(Clock24[11,0,0],Clock24["Hallo",0,0])=>Err, clock_add(Clock24[11,0,0],Clock24[23,"Hallo",0])=>Err, 
# clock_add(Clock24[11,0,0],Clock24[23,0,"Hallo"])=>Err, clock_add(Clock24[11,0,0],ClockSec[86400])=>Err, 
# clock_add(Clock24[11,0,0],ClockSec["Hallo"])=>Err, clock_add(Clock24[11,0,0],ClockSec[12.0])=>Err, 
# clock_add(Clock24[11,0,0],ClockSec[-43200])=>Err, clock_add(ClockSec[39600],Clock12[:AM,13,0,0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,13,0,0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,60,0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,60,0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,0,60])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,0,60])=>Err, 
# clock_add(ClockSec[39600],Clock12[:AM,12.0,0,0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12.0,0,0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,0.0,0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,0.0,0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,0,0.0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,0,0.0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,"Hallo",0,0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,"Hallo",0,0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,"Hallo",0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,"Hallo",0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,0,"Hallo"])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,-12,0,0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,-12,0,0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,-1,0])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,-1,0])=>Err,
# clock_add(ClockSec[39600],Clock12[:AM,12,0,-1])=>Err, clock_add(ClockSec[39600],Clock12[:PM,12,0,-1])=>Err,
# clock_add(ClockSec[39600],Clock24[24,0,0])=>Err, clock_add(ClockSec[39600],Clock24[23,60,0])=>Err,
# clock_add(ClockSec[39600],Clock24[23,0,60])=>Err, clock_add(ClockSec[39600],Clock24[-23,0,0])=>Err,
# clock_add(ClockSec[39600],Clock24[23,-1,0])=>Err, clock_add(ClockSec[39600],Clock24[23,0,-1])=>Err,
# clock_add(ClockSec[39600],Clock24[23.0,0,0])=>Err, clock_add(ClockSec[39600],Clock24[23,59.0,0])=>Err,
# clock_add(ClockSec[39600],Clock24[23,0,59.0])=>Err, clock_add(ClockSec[39600],Clock24["Hallo",0,0])=>Err,
# clock_add(ClockSec[39600],Clock24[23,"Hallo",0])=>Err, clock_add(ClockSec[39600],Clock24[23,0,"Hallo"])=>Err,
# clock_add(ClockSec[39600],ClockSec[86400])=>Err, clock_add(ClockSec[39600],ClockSec["Hallo"])=>Err, 
# clock_add(ClockSec[39600],ClockSec[12.0])=>Err, clock_add(ClockSec[39600],ClockSec[-43200])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,13,0,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,13,0,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,60,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,60,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,0,60])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,0,60])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12.0,0,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12.0,0,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,0.0,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,0.0,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,0,0.0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,0,0.0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,"Hallo",0,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,"Hallo",0,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,"Hallo",0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,"Hallo",0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,0,"Hallo"])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,-12,0,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,-12,0,0])=>Err, 
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,-1,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,-1,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock12[:AM,12,0,-1])=>Err, clock_add(Clock12[:AM,11,0,0],Clock12[:PM,12,0,-1])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock24[24,0,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock24[23,60,0])=>Err, 
# clock_add(Clock12[:AM,11,0,0],Clock24[23,0,60])=>Err, clock_add(Clock12[:AM,11,0,0],Clock24[-23,0,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock24[23,-1,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock24[23,0,-1])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock24[23.0,0,0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock24[23,59.0,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock24[23,0,59.0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock24["Hallo",0,0])=>Err,
# clock_add(Clock12[:AM,11,0,0],Clock24[23,"Hallo",0])=>Err, clock_add(Clock12[:AM,11,0,0],Clock24[23,0,"Hallo"])=>Err, 
# clock_add(Clock12[:AM,11,0,0],ClockSec[86400])=>Err, clock_add(Clock12[:AM,11,0,0],ClockSec["Hallo"])=>Err,
# clock_add(Clock12[:AM,11,0,0],ClockSec[12.0])=>Err, clock_add(Clock12[:AM,11,0,0],ClockSec[-43200])}

#def clock_add (clock1,clock2)
#  clock1_temp = check_clock1(clock1)
#  clock2_temp = check_clock2(clock2)
#  clock_new = clock_sec_add(clock1_temp,clock2_temp)
#  
#  if clock1.clock12? then
#    clock_sec_to_clock_12(clock_new)
#  elsif clock1.clock24? then
#    clock_sec_to_clock_24(clock_new)
#  else clock_new
#  end
#end
  

def clock_add(clock1,clock2) 
  to_clock(clock1,(clock_sec_add(to_clock_sec(clock1),to_clock_sec(clock2))))
end

#clock_sub ::= (clock1,clock2) ::
#                               (Clock24 x Clock -> Clock24 |
#                                Clock12 x Clock -> Clock12 |
#                                ClockSec x Clock -> ClockSec)
#Test { clock_sub(ClockSec[39600], ClockSec[3600])=>ClockSec[36000], clock_sub(ClockSec[39600]=>ClockSec[36000], Clock12[:AM,1,0,0])=>ClockSec[36000],
# clock_sub(ClockSec[39600], Clock24[1,0,0])=>ClockSec[36000], clock_sub(Clock24[11,0,0], ClockSec[3600])=>Clock24[10,0,0],
# clock_sub(Clock24[10,0,0], ClockSec[3600])=>Clock24[11,0,0], clock_sub(Clock24[11,0,0], Clock12[:AM,1,0,0])=>Clock24[11,0,0],
# clock_sub(Clock24[11,0,0], Clock24[1,0,0])=>Clock24[11,0,0], clock_sub(Clock12[:AM,11,0,0], ClockSec[3600])=>Clock12[:AM,11,0,0],
# clock_sub(Clock12[:AM,11,0,0], Clock12[:AM,1,0,0])=>Clock12[:AM,11,0,0], clock_sub(Clock12[:AM,11,0,0], Clock24[1,0,0])=>Clock12[:AM,11,0,0],
# clock_sub(Clock24[11,0,0],Clock12[:AM,13,0,0]))=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,13,0,0])=>Err, 
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,60,0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,60,0])=>Err,
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,0,60])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,0,60])=>Err, 
# clock_sub(Clock24[11,0,0],Clock12[:AM,12.0,0,0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12.0,0,0])=>Err, 
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,0.0,0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,0.0,0])=>Err, 
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,0,0.0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,0,0.0])=>Err,
# clock_sub(Clock24[11,0,0],Clock12[:AM,"Hallo",0,0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,"Hallo",0,0])=>Err,
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,"Hallo",0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,"Hallo",0])=>Err,
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,0,"Hallo"])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_sub(Clock24[11,0,0],Clock12[:AM,-12,0,0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,-12,0,0])=>Err, 
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,-1,0])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,-1,0])=>Err,
# clock_sub(Clock24[11,0,0],Clock12[:AM,12,0,-1])=>Err, clock_sub(Clock24[11,0,0],Clock12[:PM,12,0,-1])=>Err,
# clock_sub(Clock24[11,0,0],Clock24[24,0,0])=>Err, clock_sub(Clock24[11,0,0],Clock24[23,60,0])=>Err,
# clock_sub(Clock24[11,0,0],Clock24[23,0,60])=>Err, clock_sub(Clock24[11,0,0],Clock24[-23,0,0])=>Err,
# clock_sub(Clock24[11,0,0],Clock24[23,-1,0])=>Err, clock_sub(Clock24[11,0,0],Clock24[23,0,-1])=>Err, clock_sub(Clock24[11,0,0],Clock24[23.0,0,0])=>Err,
# clock_sub(Clock24[11,0,0],Clock24[23,59.0,0])=>Err, clock_sub(Clock24[11,0,0],Clock24[23,0,59.0])=>Err, 
# clock_sub(Clock24[11,0,0],Clock24["Hallo",0,0])=>Err, clock_sub(Clock24[11,0,0],Clock24[23,"Hallo",0])=>Err, 
# clock_sub(Clock24[11,0,0],Clock24[23,0,"Hallo"])=>Err, clock_sub(Clock24[11,0,0],ClockSec[86400])=>Err, 
# clock_sub(Clock24[11,0,0],ClockSec["Hallo"])=>Err, clock_sub(Clock24[11,0,0],ClockSec[12.0])=>Err, 
# clock_sub(Clock24[11,0,0],ClockSec[-43200])=>Err, clock_sub(ClockSec[39600],Clock12[:AM,13,0,0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,13,0,0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,60,0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,60,0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,0,60])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,0,60])=>Err, 
# clock_sub(ClockSec[39600],Clock12[:AM,12.0,0,0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12.0,0,0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,0.0,0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,0.0,0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,0,0.0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,0,0.0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,"Hallo",0,0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,"Hallo",0,0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,"Hallo",0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,"Hallo",0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,0,"Hallo"])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,-12,0,0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,-12,0,0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,-1,0])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,-1,0])=>Err,
# clock_sub(ClockSec[39600],Clock12[:AM,12,0,-1])=>Err, clock_sub(ClockSec[39600],Clock12[:PM,12,0,-1])=>Err,
# clock_sub(ClockSec[39600],Clock24[24,0,0])=>Err, clock_sub(ClockSec[39600],Clock24[23,60,0])=>Err,
# clock_sub(ClockSec[39600],Clock24[23,0,60])=>Err, clock_sub(ClockSec[39600],Clock24[-23,0,0])=>Err,
# clock_sub(ClockSec[39600],Clock24[23,-1,0])=>Err, clock_sub(ClockSec[39600],Clock24[23,0,-1])=>Err,
# clock_sub(ClockSec[39600],Clock24[23.0,0,0])=>Err, clock_sub(ClockSec[39600],Clock24[23,59.0,0])=>Err,
# clock_sub(ClockSec[39600],Clock24[23,0,59.0])=>Err, clock_sub(ClockSec[39600],Clock24["Hallo",0,0])=>Err,
# clock_sub(ClockSec[39600],Clock24[23,"Hallo",0])=>Err, clock_sub(ClockSec[39600],Clock24[23,0,"Hallo"])=>Err,
# clock_sub(ClockSec[39600],ClockSec[86400])=>Err, clock_sub(ClockSec[39600],ClockSec["Hallo"])=>Err, 
# clock_sub(ClockSec[39600],ClockSec[12.0])=>Err, clock_sub(ClockSec[39600],ClockSec[-43200])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,13,0,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,13,0,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,60,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,60,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,0,60])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,0,60])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12.0,0,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12.0,0,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,0.0,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,0.0,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,0,0.0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,0,0.0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,"Hallo",0,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,"Hallo",0,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,"Hallo",0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,"Hallo",0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,0,"Hallo"])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,-12,0,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,-12,0,0])=>Err, 
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,-1,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,-1,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock12[:AM,12,0,-1])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock12[:PM,12,0,-1])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock24[24,0,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock24[23,60,0])=>Err, 
# clock_sub(Clock12[:AM,11,0,0],Clock24[23,0,60])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock24[-23,0,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock24[23,-1,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock24[23,0,-1])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock24[23.0,0,0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock24[23,59.0,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock24[23,0,59.0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock24["Hallo",0,0])=>Err,
# clock_sub(Clock12[:AM,11,0,0],Clock24[23,"Hallo",0])=>Err, clock_sub(Clock12[:AM,11,0,0],Clock24[23,0,"Hallo"])=>Err, 
# clock_sub(Clock12[:AM,11,0,0],ClockSec[86400])=>Err, clock_sub(Clock12[:AM,11,0,0],ClockSec["Hallo"])=>Err,
# clock_sub(Clock12[:AM,11,0,0],ClockSec[12.0])=>Err, clock_sub(Clock12[:AM,11,0,0],ClockSec[-43200])}

def clock_sub(clock1,clock2) 
  to_clock(clock1,(clock_sec_sub(to_clock_sec(clock1),to_clock_sec(clock2))))
end

#clock_succ ::= (clock) ::
#                       (Clock24 <-> Clock24 |
#                        Clock12 <-> Clock12 |
#                        ClockSec <-> ClockSec)
#
#Test {clock_succ(ClockSec[39600])=>ClockSec[39601],clock_succ(Clock12[:AM,1,0,0])=>Clock12[:AM,1,0,1],
# clock_succ(Clock24[1,0,0])=>Clock24[1,0,1], clock_succ(Clock12[:AM,13,0,0])=>Err, 
# clock_succ(Clock12[:PM,13,0,0])=>Err, clock_succ(Clock12[:AM,12,60,0])=>Err, clock_succ(Clock12[:PM,12,60,0])=>Err,
# clock_succ(Clock12[:AM,12,0,60])=>Err, clock_succ(Clock12[:PM,12,0,60])=>Err, clock_succ(Clock12[:AM,12.0,0,0])=>Err,
# clock_succ(Clock12[:PM,12.0,0,0])=>Err, clock_succ(Clock12[:AM,12,0.0,0])=>Err, clock_succ(Clock12[:PM,12,0.0,0])=>Err,
# assert_raise(RuntimeError){clock_succ(Clock12[:AM,12,0,0.0])=>Err, clock_succ(Clock12[:PM,12,0,0.0])=>Err,
# clock_succ(Clock12[:AM,"Hallo",0,0])=>Err, clock_succ(Clock12[:PM,"Hallo",0,0])=>Err, 
# clock_succ(Clock12[:AM,12,"Hallo",0])=>Err, clock_succ(Clock12[:PM,12,"Hallo",0])=>Err, 
# clock_succ(Clock12[:AM,12,0,"Hallo"])=>Err, clock_succ(Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_succ(Clock12[:AM,-12,0,0])=>Err, clock_succ(Clock12[:PM,-12,0,0])=>Err, clock_succ(Clock12[:AM,12,-1,0])=>Err,
# clock_succ(Clock12[:PM,12,-1,0])=>Err, clock_succ(Clock12[:AM,12,0,-1])=>Err, clock_succ(Clock12[:PM,12,0,-1])=>Err,
# clock_succ(Clock12[:AM,13,0,0])=>Err, clock_succ(Clock12[:PM,13,0,0])=>Err, clock_succ(Clock12[:AM,12,60,0])=>Err,
# clock_succ(Clock12[:PM,12,60,0])=>Err, clock_succ(Clock12[:AM,12,0,60])=>Err, clock_succ(Clock12[:PM,12,0,60])=>Err,
# clock_succ(Clock12[:AM,12.0,0,0])=>Err, clock_succ(Clock12[:PM,12.0,0,0])=>Err, clock_succ(Clock12[:AM,12,0.0,0])=>Err,
# clock_succ(Clock12[:PM,12,0.0,0])=>Err, clock_succ(Clock12[:AM,12,0,0.0])=>Err, clock_succ(Clock12[:PM,12,0,0.0])=>Err,
# clock_succ(Clock12[:AM,"Hallo",0,0])=>Err, clock_succ(Clock12[:PM,"Hallo",0,0])=>Err, clock_succ(Clock12[:AM,12,"Hallo",0])=>Err,
# clock_succ(Clock12[:PM,12,"Hallo",0])=>Err, clock_succ(Clock12[:AM,12,0,"Hallo"])=>Err,clock_succ(Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_succ(Clock12[:AM,-12,0,0])=>Err, clock_succ(Clock12[:PM,-12,0,0])=>Err, clock_succ(Clock12[:AM,12,-1,0])=>Err,
# clock_succ(Clock12[:PM,12,-1,0])=>Err, clock_succ(Clock12[:AM,12,0,-1])=>Err, clock_succ(Clock12[:PM,12,0,-1])=>Err,
# clock_succ(Clock24[24,0,0])=>Err, clock_succ(Clock24[23,60,0])=>Err, clock_succ(Clock24[23,0,60])=>Err,
# clock_succ(Clock24[-23,0,0])=>Err, clock_succ(Clock24[23,-1,0])=>Err, clock_succ(Clock24[23,0,-1])=>Err,
# clock_succ(Clock24[23.0,0,0])=>Err, clock_succ(Clock24[23,59.0,0])=>Err, clock_succ(Clock24[23,0,59.0])=>Err,
# clock_succ(Clock24["Hallo",0,0])=>Err, clock_succ(Clock24[23,"Hallo",0])=>Err, clock_succ(Clock24[23,0,"Hallo"])=>Err,
# clock_succ(ClockSec[86400])=>Err, clock_succ(ClockSec["Hallo"])=>Err, clock_succ(ClockSec[12.0])=>Err, clock_succ(ClockSec[-43200])=Err}

def clock_succ(clock1) 
  to_clock(clock1,(clock_sec_succ(to_clock_sec(clock1))))
end

#clock_pred ::= (clock) ::
#                         (Clock24 <-> Clock24 |
#                          Clock12 <-> Clock12 |
#                          ClockSec <-> ClockSec)
#
#Test {clock_pred(ClockSec[39601])=>ClockSec[39600],clock_pred(Clock12[:AM,1,0,1])=>Clock12[:AM,1,0,0],
# clock_pred(Clock24[1,0,1])=>Clock24[1,0,0], clock_pred(Clock12[:AM,13,0,0])=>Err, 
# clock_pred(Clock12[:PM,13,0,0])=>Err, clock_pred(Clock12[:AM,12,60,0])=>Err, clock_pred(Clock12[:PM,12,60,0])=>Err,
# clock_pred(Clock12[:AM,12,0,60])=>Err, clock_pred(Clock12[:PM,12,0,60])=>Err, clock_pred(Clock12[:AM,12.0,0,0])=>Err,
# clock_pred(Clock12[:PM,12.0,0,0])=>Err, clock_pred(Clock12[:AM,12,0.0,0])=>Err, clock_pred(Clock12[:PM,12,0.0,0])=>Err,
# assert_raise(RuntimeError){clock_pred(Clock12[:AM,12,0,0.0])=>Err, clock_pred(Clock12[:PM,12,0,0.0])=>Err,
# clock_pred(Clock12[:AM,"Hallo",0,0])=>Err, clock_pred(Clock12[:PM,"Hallo",0,0])=>Err, 
# clock_pred(Clock12[:AM,12,"Hallo",0])=>Err, clock_pred(Clock12[:PM,12,"Hallo",0])=>Err, 
# clock_pred(Clock12[:AM,12,0,"Hallo"])=>Err, clock_pred(Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_pred(Clock12[:AM,-12,0,0])=>Err, clock_pred(Clock12[:PM,-12,0,0])=>Err, clock_pred(Clock12[:AM,12,-1,0])=>Err,
# clock_pred(Clock12[:PM,12,-1,0])=>Err, clock_pred(Clock12[:AM,12,0,-1])=>Err, clock_pred(Clock12[:PM,12,0,-1])=>Err,
# clock_pred(Clock12[:AM,13,0,0])=>Err, clock_pred(Clock12[:PM,13,0,0])=>Err, clock_pred(Clock12[:AM,12,60,0])=>Err,
# clock_pred(Clock12[:PM,12,60,0])=>Err, clock_pred(Clock12[:AM,12,0,60])=>Err, clock_pred(Clock12[:PM,12,0,60])=>Err,
# clock_pred(Clock12[:AM,12.0,0,0])=>Err, clock_pred(Clock12[:PM,12.0,0,0])=>Err, clock_pred(Clock12[:AM,12,0.0,0])=>Err,
# clock_pred(Clock12[:PM,12,0.0,0])=>Err, clock_pred(Clock12[:AM,12,0,0.0])=>Err, clock_pred(Clock12[:PM,12,0,0.0])=>Err,
# clock_pred(Clock12[:AM,"Hallo",0,0])=>Err, clock_pred(Clock12[:PM,"Hallo",0,0])=>Err, clock_pred(Clock12[:AM,12,"Hallo",0])=>Err,
# clock_pred(Clock12[:PM,12,"Hallo",0])=>Err, clock_pred(Clock12[:AM,12,0,"Hallo"])=>Err,clock_pred(Clock12[:PM,12,0,"Hallo"])=>Err,
# clock_pred(Clock12[:AM,-12,0,0])=>Err, clock_pred(Clock12[:PM,-12,0,0])=>Err, clock_pred(Clock12[:AM,12,-1,0])=>Err,
# clock_pred(Clock12[:PM,12,-1,0])=>Err, clock_pred(Clock12[:AM,12,0,-1])=>Err, clock_pred(Clock12[:PM,12,0,-1])=>Err,
# clock_pred(Clock24[24,0,0])=>Err, clock_pred(Clock24[23,60,0])=>Err, clock_pred(Clock24[23,0,60])=>Err,
# clock_pred(Clock24[-23,0,0])=>Err, clock_pred(Clock24[23,-1,0])=>Err, clock_pred(Clock24[23,0,-1])=>Err,
# clock_pred(Clock24[23.0,0,0])=>Err, clock_pred(Clock24[23,59.0,0])=>Err, clock_pred(Clock24[23,0,59.0])=>Err,
# clock_pred(Clock24["Hallo",0,0])=>Err, clock_pred(Clock24[23,"Hallo",0])=>Err, clock_pred(Clock24[23,0,"Hallo"])=>Err,
# clock_pred(ClockSec[86400])=>Err, clock_pred(ClockSec["Hallo"])=>Err, clock_pred(ClockSec[12.0])=>Err, clock_pred(ClockSec[-43200])=Err}

def clock_pred(clock1) 
  to_clock(clock1,(clock_sec_pred(to_clock_sec(clock1))))
end

#Vergleich von 2 Uhren
#clock_equal? ::= (obj1,obj2) :: (Clock x Clock -> Bool |
#                                 Clock x (Any - Clock) -> False |
#                                (Any - Clock) x Clock -> False |
#                                (Any - Clock) x (Any - Clock) -> Err)

def clock_equal(value1, value2)
  if is_clock(value1) and is_clock(value2) then
    (to_clock_sec(value1) == to_clock_sec(value2))
  elsif not is_clock(value1) or not is_clock(value2) then
    false
  else
    check_pre((false))
  end
end

def is_clock(value)
  (value.clock12? or value.clock24? or value.clock_sec?)
end